A:Type, F:(A), L:(A List). (k:A. Dec(F(k)))  Dec(kL. F(k)) 

latex

Definitions

P  Q, x:A. B(x), Dec(P), Type, t  T, s = t, , x:AB(x), type List, f(a), x(s), P  Q, , x.A(x), inr x , outl(x), inl x , tt, p  q, reduce(f;k;as), if b then t else f fi , b, (x  l), A, [], left + right, Decision, xL. P(x), x:A  B(x), x:A. B(x), tl(l), n - m, if a<b then c else d, i <z j, b, i z j, nth_tl(n;as), hd(l), l[i], n+m, rec-case(a) of [] => s | x::y => z.t(x;y;z), Y, ||as||, a < b, A  B, , {x:A| B(x)} , , case b of inl(x) => s(x) | inr(y) => t(y), isl(x), p =b q, (i = j), x =a y, null(as), a < b, x f y, a < b, [d], p  q, p q, b | a, a ~ b, a  b, a <p b, a < b, A c B, (xL.P(x)), False, P  Q, P & Q, P  Q, {T}, , ff, s ~ t, SQType(T), x. t(x), [car / cdr], Void, Unit, #$n, True

Lemmas

l all cons, l all wf, cons member, it wf, l all wf2, bnot wf, bool wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, false wf, bool sq, bool cases, bfalse wf, btrue wf, nil member, decidable assert, isl wf, outl wf, not wf, l member wf, assert wf, decidable wf